\begin{tipo}{MinisterioDeTurismo}
	\observador{secretarias}{m: MinisterioDeTurismo}{[Provincia]}
	\observador{registro}{m: MinisterioDeTurismo, p: Provincia }{[Hotel]}
	\requiere{p \in secretarias(m)}
	\observador{cadenasDeHoteles}{m: MinisterioDeTurismo}{[[Hotel]]}	
	\invariante[sinHotelesRepetidas]{(\forall xs \selec cadenasDeHoteles(m)) sinRepetidos(xs)}
	\invariante[sinCadenasRepetidas]{sinRepetidos(xs)}
	\invariante[sinProvinciasRepetidas]{sinRepetidos(secretarias(m))}
	\invariante[cadenasBienFormadas]{\input{problemas/11.tex}}
	\invariante[sinNombresRepetidosEnCadenas]{\input{problemas/12.tex}}
	\invariante[hotelesConsistentes]{\input{problemas/13.tex}}
\end{tipo}
